(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-highlight-add-annotations 'nil '(66 67 (shadowingintelescope)))
(agda2-highlight-add-annotations 'nil '(1 4 (symbol) t) '(5 12 (keyword) t) '(13 22 (pragma) t) '(23 43 (pragma) t) '(44 47 (symbol) t) '(49 58 (keyword) t) '(61 62 (symbol) t) '(63 64 (symbol) t) '(65 66 (symbol) t) '(70 71 (symbol) t) '(75 76 (symbol) t) '(77 78 (symbol) t))
(agda2-highlight-add-annotations 'nil '(61 62 (postulate) nil nil ("Issue3989.agda" . 61)) '(66 67 (bound) nil nil ("Issue3989.agda" . 66)) '(68 69 (bound) nil nil ("Issue3989.agda" . 68)) '(72 75 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(79 82 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(61 62 (postulate) nil nil ("Issue3989.agda" . 61)) '(63 64 (symbol) t) '(65 66 (symbol) t) '(66 67 (bound) nil nil ("Issue3989.agda" . 66)) '(68 69 (bound) nil nil ("Issue3989.agda" . 68)) '(70 71 (symbol) t) '(72 75 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(75 76 (symbol) t) '(77 78 (symbol) t) '(79 82 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(1 4 (symbol) t) '(5 12 (keyword) t) '(13 22 (pragma) t) '(23 43 (pragma) t) '(44 47 (symbol) t) '(49 58 (keyword) t))
(agda2-status-action "Checked")
(agda2-info-action "*All Warnings*" "Issue3989.agda:4,8-11 Shadowing in telescope, repeated variable names: A when scope checking (A A : Set) → Set " nil)
((last . 1) . (agda2-goals-action '()))
